\begin{figure}[t]
	\centering
	\begin{minipage}[t]{0.7\linewidth}
{\begingroup
\footnotesize
\begin{IEEEeqnarray*}{rCl}
\Specs & ::= & \Spec^* \\
\Spec & ::= & \textbf{\texttt{Spec: }}\Target~\Fib~\Pre~\Post~\\
\Target & ::= & \textbf{\texttt{Target: }} \FunSig \\
\Fib & ::= & \textbf{\texttt{Fib }} \\
\Pre & ::= & \textbf{\texttt{Pre: }} \Cond^+ \\
\Post & ::= & \textbf{\texttt{Post: }} (\Cond \texttt{,} \Action^*)^+ \\
\Cond & ::= & \true \mid \Opd~\CmpOp~\Opd \mid \Opd~\MemberOp~\texttt{(}\Set \texttt{)} \\
\Action & ::= & \Return \mid \Call   \\
\Return & ::= & \ReturnFun{\FunName:n} \mid \ReturnFun{\FunName:\NULL} \\
\Call & ::= & \CallFun{\FunName \texttt{:} \Cond^*} \\
\Opd & ::= & \Arg \mid \UnOp\texttt{(}\Arg\texttt{)} \mid \textbf{\NULL} \mid n\\
% funName(type*) -> function may have no parameter
\FunSig & ::= & \FunName \texttt{(} \Type^* \texttt{)}~\texttt{->}~ \Type \\  
\Arg & ::= & \FunName \textbf{\texttt{\_arg\_}} i \\
\UnOp & ::= & \textbf{\LEN} \mid \textbf{\TYPE} \mid \textbf{\MEMTYPE} \\
\CmpOp & ::= & \textbf{\texttt{!=}} \mid \textbf{\texttt{==}} \mid \textbf{\texttt{>=}} \mid \textbf{\texttt{>}} \mid \textbf{\texttt{<=}} \mid \textbf{\texttt{<}} \\
\MemberOp & ::= & \textbf{\IN} \mid \textbf{\NOTIN} \\
\Set & ::= & \myid^+ \mid [n_1:n_2]^+ \\
\FunName & ::= & \myid \\
\Type & ::= & \myid
\end{IEEEeqnarray*}
	\endgroup
	}
	\setlength{\abovecaptionskip}{-10pt}
	\caption{IMSpec语法结构}
	\label{fig:2-4-syntax}
		\end{minipage}
\end{figure}
